Nuprl Lemma : list_append
2,24
postcript
pdf
T
:Type,
as
,
bs
:
T
List. (
as
@
bs
)
T
List
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
origin
T:Type, as, bs:T List. (as @ bs) 
T List T:Type, as, bs:T List. (as @ bs) T List x:A. B(x) T